package cfsmon.logic.nfm;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;

import cfsmon.common.Event;

/**
 * The state of a nondeterministic finite state machine. It consist of a name and outgoing
 * transitions. The transitions are modeled as a relation between events and target states.
 * The concept of a 'default transition' completes the transition relation in the following
 * way: If the set of default transitions is empty every event that does not cause a
 * transition into another state causes a reflexive transition. If the set of default
 * transitions is non-empty, every event that does not cause any transition into another
 * state (with respect to the non-default relation) causes a transition into all states in
 * the default transition set.
 * @author Alexander Gebhardt
 *
 */
public class NfmState {

	private String name;
	private Map<Event, Set<NfmState>> transitions;
	private Set<NfmState> defaultTransition;
	
	public NfmState(String name) throws IllegalArgumentException{
		super();
		if (name == null)
			throw new IllegalArgumentException("A null string is not allowed as state name.");
		this.name = name;
		this.transitions = new HashMap<Event, Set<NfmState>>();
		defaultTransition = new HashSet<NfmState>();
	}

	public String getName() {
		return name;
	}
	
	/**
	 * Adds a transition from this state to a target state triggered by an event.
	 * @param e an event
	 * @param to the target state
	 * @throws IllegalArgumentException if at least one parameter is null
	 */
	public void putTransition(Event e, NfmState to) throws IllegalArgumentException{
		if (e == null || to == null)
			throw new IllegalArgumentException("Invalid parameters to putTransition call of a state");
		Set<NfmState> toSet = transitions.get(e);
		if (toSet == null){
			toSet = new HashSet<NfmState>();
			transitions.put(e, toSet);
		}
		toSet.add(to);
	}
	
	public Map<Event, Set<NfmState>> getTransitions(){
		return transitions;
	}
	
	public Set<NfmState> getDefaultTransition(){
		return defaultTransition;
	}
	
	public void addDefaultTransition(NfmState t) throws IllegalArgumentException{
		if (t == null)
			throw new IllegalArgumentException("Invalid parameters to addDefaultTransition call of a state");
		defaultTransition.add(t);
	}
	
	@Override
	public String toString(){
		return name;
	}
	
	public String toStringDeep(){
		StringBuffer sb = new StringBuffer();
		for (Event e : transitions.keySet()){
			for (NfmState to : transitions.get(e)){
				sb.append("(" + this + ", " + e + ", " + to + ") in Delta\n");
			}
		}
		for (NfmState to : defaultTransition){
			sb.append("forall e in Events. NEx s in States where (" + this + ", e, s) in Delta implies ("+ this + ", e, " + to + ") in Delta'\n");
		}
		return sb.toString();
	}
	
	public void printDeep(){
		System.out.print(toStringDeep());
	}
	
}
